Metamath Blueprint : Triangle Congruences

Geometry

This project follows closely Schwabenhaeuser.

See set.mm#2983:

We do have all 3 segment versions of CPCTC, namely cgr3simp1, cgr3simp2, and cgr3simp3; we're just missing two of the CPCTC angle forms.

SAS is already proven in tgsas1 and tgsas. ASA is proven in tgasa1 and tgasa. We don't actually have a proof of AAS (Angle-Angle-Side), Theorem 11.50 of [Schwabhauser] p. 108, we just have a placeholder.

---